System F
二階ラムダ計算 や 多相ラムダ計算 として知られる｡またこれを型システムに埋め込むことで強力な型を表現できる｡
簡単な例として､よくある id 関数をSystem Fで表すとこのようになる｡
$ \mathit{id} = \Lambda a. \lambda x : a. x \rightarrow x
$ xの型を$ aでパラメタライズ することで多相性 を獲得している｡
しかし二階ラムダ計算なので型パラメータに二階の型を取ることができない｡では三階ラムダ計算はあるのかと言われると(多分)無い｡
三階以上はもはや青天井と見なしてよいので､System F$ \omega という無限階のラムダ計算になる｡
System Fを利用した型システムの型推論は(アノテーションが無いと)決定不能になる｡
アノテーションが無いと型推論が決定不能なのはユーザにとってだいぶ面倒なので､もう少し制限することで決定可能にしたい｡
System F制限を加えてアノテーションがなくても決定可能な型推論ができる型システムがHindley-Milner型システムである｡HM型システムはML方言やHaskellなどの型システムの基礎となっている｡
references